\documentclass[11pt,draft,oneside]{fithesis}
%default packages
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}  % for unicode UTF-8
\usepackage[plainpages=false, colorlinks, pdfpagelabels]{hyperref}

%added packages
\usepackage{booktabs} % for much better looking tables
\usepackage{array} % for better arrays (eg matrices) in maths
\usepackage{paralist} % very flexible & customisable lists (eg. enumerate/itemize, etc.)
\usepackage{verbatim} % adds environment for commenting out blocks of text & for better verbatim
\usepackage{subfig} % make it possible to include more than one captioned figure/table in a single float
\usepackage{pgfplots}
\usepackage{csquotes}
\usepackage[backend=biber,maxbibnames=99,sortcites=true,url=true,hyperref=true]{biblatex}
\usepackage{enumitem}
\usepackage{tabto}
\usepackage{amsmath}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{tikz}

%thesis settings:
\thesislang{en}
\thesistitle{Trading space for time in explicit-state model checking}
\thesissubtitle{Diploma Thesis}
\thesisstudent{Pavel Mičan}
\thesiswoman{false}
\thesisfaculty{fi}
\thesisyear{Spring 2013}
\thesisadvisor{Jiří Barnat}

%added settings:
\pgfplotsset{compat=1.7}
\addbibresource{mybib.bib}

\pretolerance=300 %increased paragraph spacing because of the URLs in bibiliography
\tolerance=600

\setlist[itemize]{noitemsep}
\setlist[enumerate]{noitemsep}

\usetikzlibrary{arrows, automata, positioning, trees}

\newtheorem{statement}{Statement}[section]

\tikzset{
    %Define style for states
    state/.style={
           circle,
           draw=black,
           very thick,
           minimum height=2em,
           text centered},
    pthState/.style={
           circle,
           draw=black,
           very thick,
           minimum height=2em,
           color=red,
           text centered},
    pathBegin/.style={edge from parent/.style={red,very thick,draw}},
    pathEnd/.style={edge from parent/.style={black,very thick,draw}}
}

\begin{document}
\FrontMatter
\ThesisTitlePage

\begin{ThesisDeclaration}
\DeclarationText
\AdvisorName
\end{ThesisDeclaration}

\begin{ThesisThanks} \begin{itshape} If the bricks aren't well made, the wall
falls down. 

This is an awfully big wall I'm building here, so I need a lot of bricks.
Fortunately I know a lot of brickmakers, and all sorts of other folks as well.
\par \hfill [George R.R. Martin] \end{itshape}

\bigskip

Thanks and appreciation to all good people who guided me through the tough time
of understanding the depths of DiVinE model checker, to those who stood by me in
my frequent states of despair and my special thanks to my supervisor Jiří
Barnat, who must have grown hair only to lose them again waiting for my
progress.  \end{ThesisThanks}

\begin{ThesisAbstracten} To reduce the memory size requirements in accepting
cycle detection algorithms we came with an approach of storing only certain
states based on their ordering. A random assignment of an integer value (ideally
unique) is given to each state and while processing en edge of a graph only
those states are stored which have its assigned value lower to the maximum value
found since the last state had been stored. This simple solution trades memory
space for computing time and is applicable to various DFS and even BFS
on-the-fly algorithms. In this thesis I present the detailed description of the
technique along with it's correctness prove. I additionally implemented the
algorithm into the DiVinE model checking tool and measurements of it's
efficiency are included at the end of the work.  \end{ThesisAbstracten}

\begin{ThesisKeyWords} model checking, verification, distributed, to store or
not to store, OWCTY, Nested DFS, DiVinE \end{ThesisKeyWords} 

\MainMatter \tableofcontents


%%%BEGINNING:%%%

\chapter{Introduction} Model checking \cite{modelChecking} is a well established
method of formal verification with increasing popularity. The use of Model
checking is becoming crucial for verifying correctness properties of hardware
and software systems or protocols that require high level of reliability, and it
has become an integrated part of the verification process in many companies such
as IBM who maintain RuleBase symbolic model checking tool
\cite{IBMmch,mchIBMGigahertzProcessor}, Microsoft's Static Driver Verifier (SDV)
\cite{website:MS:SDV} developed as a part of the SLAM project
\cite{mchMicrosoft} that recently successfully demonstrated a computer-aided
verification on real programs \cite{Ball:2011:DSM:1965724.1965743,
slamTwoLowFalseAlarm}, well known SPIN tool developed at Bell Labs
\cite{website:SPIN}, and many others\cite{fvInSysDesign, HWFDesignMethodology,
IBMfvCoreconnect, wiki:mct}, and in addition to all these a DiVinE model
checker\cite{DiVinE, website:DiVinE} is being developed in the laboratory of
Parallel and Distributed Systems (ParaDiSe) \cite{website:ParaDiSe}.

At the moment the DiVinE model checking tool provides multiple different
algorithms that traverse given graph and are capable of finding an accepting
cycle in order to prove correctness of a given property in a modelled system or
provide not only the information on it's misbehaviour, but also a counterexample
in a form of a succession of steps that lead from the initial state to a state
where the conditions are not met. Apart from the classical NestedDFS algorithm,
the DiVinE exploits breadth-first-search (BFS) algorithms such as Maximal
Accepting Predecessor (MAP) or One-Way Catch Them Young
(OWCTY)\cite{art:ClusterLTLmc,}. Detailed description to these algorithms is
discussed in Chapter 3.

Having said that, the industrial-scale models are mainly restricted by memory
size. For the past years the research in model checking was mainly concerned
with a problem commonly known as a state-space expansion. The issue is to deal
with a memory requirements which grow exponentially with the size of tested
system and/or property\cite{Hammer06tostore}. The chapter 2 is dedicated to
explain what the explicit state space model checking is and how does a property
checking lead to the expansion problem.

The aim of the technique presented in this work is to provide a simple solution
to reduce memory consumption that would be independent of an algorithm used to
traverse the given graph and also allow the DiVinE model checker use it's
distributing algorithm potential. To do that, the method used must be able to
work with on-the-fly algorithms, ie. algorithms that dynamically pass through a
given graph searching for an accepting cycle. To represent it's effectiveness, I
tested the code implemented in DiVinE using two DFS algorithms, namely NestedDFS
and reachability, and MAP together with OWCTY were used as BFS algorithm
representatives. Yet, the results are not a part of this edition for the lack
of their credibility, for the implementation at the moment does not ensure the
correct behaviour and in various models triggers segmentation faults.

At the beginning of the work I present a brief insight into the Model Checking
phenomenon and explain the procedure leading to the state explosion problem.

The third chapter is then fully dedicated to the new technique.

At the very end of the thesis assumptions on further expansions of the
technique and possible research are stated.




\chapter{Model Checking and State Explosion Problem}
To address the problem of state explosion in LTL model checking it is crucial to
understand two essential structures. First, the model of a tested system
represented as B\"uchi automatons (BA)\cite{Thomas:AutomataInfObj,}, and second
the Linear Temporal Logic (LTL) expressions again transformed into a BA.

Having these two basic structures, we may claim that a model satisfies LTL
formul\ae\ if and only if the language of the system model is a subset of the
language of a given LTL formula. This conclusion is described in more detail at
the end of this chapter in the Big Bang section. But first, let me introduce
the two basic structures.

\section{System model}
The system model is an oriented graph representation of the system we'd like to
test. The model is based on Kripke Structure (KS) \cite{modelChecking,
baier2008principles}, which is a variation of a non-deterministic automaton.

The model being a representation of a program, it needs to reflect basic
behaviour and properties of each state in which the running program can be.
Thus, the Kripke structure is a four-tuple $(S, T, I, S_{0})$ where:
\begin{itemize}
    \item $S$ is a finite set of states in which the system can be, 
    \item $T \subseteq S \times S$ is a transition relation that must be total,
    and represents transitions from one state to another,
    \item $I : S \rightarrow 2^{AP}$ is an interpretation that assigns each 
                        state a set of valid atomic propositions,
    \item $S_{0}$ is a set of initial states.
\end{itemize}
The interpretation $I$ in the structure expresses certain qualities of inner
state properties. An example of an atomic proposition might be strictly
defined, eg. "$x = 4$" implies that in the state containing this AP the value
of $x$ is exactly four, but AP might even assert a range of possible values,
eg. "$x < 5$" or "$min(x,y,z) > 0$". In general, an atomic proposition is any
statement that can be easily tested by a machine and restricts values of
properties that appear in the modelled system.

The Kripke Structure can be easily transformed into a Kripke Transition System
by adding fifth element $L : T \rightarrow Act$ of labels. The labels assign a
set of actions $Act$ the program may execute to each transition.

Having the system structure defined there is only a small step needed to be
able to automatically decide whether the system run has desired quality. The
formalism of B\"uchi Automaton (BA) gives us an ability to walk through the
infinite system and decide the acceptance. Let $(S, T, I, S_{0})$ be a Kripke
structure, then the BA $(\Sigma, S_{B}, s_{0}, \delta, F)$ is constructed as
follows:
\begin{enumerate}
    \item $\Sigma = 2^{AP}$ 
    \item $S_{B} = S \cup \{s_{0}\}$
    \item $s_{0}$ is a new initial state, ie. $s_{0} \cap S = \emptyset$
    \item $\delta$ is defined as follows:
    \begin{itemize}
        \item $(s, \alpha, s') \in \delta for s, s' \in S iff (s, s') \in T
        \wedge \alpha = I(s')$ and
        \item $(s_{0}, \alpha, s) \in \delta iff s \in S \wedge \alpha = I(s)$
    \end{itemize}
    \item $F = S \cup \{s_{0}\}$
\end{enumerate}


\section{LTL formul\ae}
In this section I will describe in short what the LTL formula is and then outline
the process of its' transformation into a B\"uchi automaton. 

\subsection{LTL definition}
Using the Linear (or Linear-Time) Temporal Logic expressions one can
describe assertions of system paths. In Temporal Logic we define following operators:
\begin{itemize}
    \item $F \varphi$ \tabto{1.0cm} -- somewhere in the $\bf F$uture the $\varphi$ is satisfied
    \item $G \varphi$ \tabto{1.0cm}  -- $\varphi$ is $\bf G$lobally satisfied
    \item $\varphi U \psi$ \tabto{1.0cm}  -- $\psi$ is certainly satisfied at some point
                                          but $\bf U$ntil then the $\varphi$ is satisfied 
    \item $X \varphi$ \tabto{1.0cm}  -- $\varphi$ is satisfied in the ne$\bf X$t state
    \item $\varphi W \psi$ \tabto{1.0cm}  -- $\bf W$eakens the Until operator by the
                                          fact that $\psi$ may not be satisfied at any point
    \item $\varphi R \psi$ \tabto{1.0cm}  -- $\psi$ is satisfied until it's $\bf R$eleased
                                          by concurrent satisfaction of $\psi \wedge \varphi$
\end{itemize}
An obvious question arise at this point. What are these $\varphi$ and $\psi$
formul\ae? From what I already described, the answer is intuitive. We already
know the set of Atomical Propositions. Now we can easily claim that every $p
\in AP$ is an LTL formula and it's satisfaction is trivially decided against
each state in the system. Then we may iteratively define \textit{negation} and
logical \textit{or} as $\neg \varphi$ and $\varphi \vee \varphi$ being formula.
The semantics of these is intuitive.

For simplicity of use, the LTL generally used is restricted to ne$X$t and
$U$ntil operators. It can be proven that all the others can be described using
these two \cite{baier2008principles}. Thus the summarized LTL syntax is:
$$\varphi ::= p | \neg\varphi | \varphi \vee \varphi | X\varphi | \varphi U
\varphi$$

\subsection{LTL into B\"uchi}
To create a B\"uchi representation of the LTL formula, all we need to achieve
is to construct a simple automaton model, and this model is nothing else than
a run of Kripke structure. That may be intuitively described as a succession of
states with such APs which reflect all possible behaviour satisfying the formula.

The exact process of transforming the formula exceeds the dimension of this
thesis, but in short, the process of the translation follows these simple steps:
\begin{enumerate}
    \item conversion of an LTL formula into a normal form
    \item computation of a transition graph
    \item conversion of the transition graph into a generalised BA (GBA)
    \item conversion of GBA into a BA
\end{enumerate}

It can be shown that all the valid LTL formul\ae\ may be transformed into the BA
following these steps\cite{baier2008principles, wiki:LTLtoBA}.


\section{The Big Bang}
In the beginning of this chapter I mentioned that the system model satisfies
the given LTL formula \textit{iff} the language of the former is a subset of the
second. Let me introduce this phenomenon in more detail and finally hit the fan
with an immense explosion!

We already have the formal description of LTL and System BA. From the automaton
theory\cite{hopcroft2001introduction} we know that an automaton accepts words
of a certain language, thus fully defines the language. The language accepted by
an automaton $A$ is denoted as $L(A)$. The crux of all the model checking is to
decide whether the system model $M$ satisfies given formula $\varphi$. As to
follow the convention, let us call the formula a \textit{property} from now on.
From what we already know it's only natural to say that the following must be true:

Let $M$ be the modelled system, $\varphi$ the given property to be verified,
$L_{sys}$ the language accepted by the system BA ($L(A_{sys})$), and
$L_{\varphi}$ the language accepted by the property BA ($L(A_{LTL})$) then
$$M\models\varphi \Longleftrightarrow L_{sys} \subseteq L_{\varphi}$$ and after
a few elemental logical transformations we may easily convert the problem onto
a test of a language emptiness:
$$M\models\varphi \Longleftrightarrow L(A_{sys}) \times L(A_{\neg\varphi})=\emptyset$$

The result of the combination of these two automatons is called a \textit{product}
and it's size entails the State Explosion Problem. The fact is that even with
relatively small system and property automatons, the product may have thousands
of states\cite{stateExplosionProblem, modelChecking, baier2008principles,
art:ClusterLTLmc, Hammer06tostore, conf:cav:storeNoStorePelanek}, and when we
expect to verify most of the real-life systems, the memory consumption really
matters and becomes the major bottleneck to the point of inability to use any
model checker.



\chapter{Algorithm}
In this chapter I'll present the dynamic algorithm, that should slightly reduce
the memory consumption while traversing the product graph.

To find a cycle in a given graph, we only need to store a single vertex on
the accepting cycle as proven in \cite{pelanekSnS}. It may be intuitive for a
trained eye, that while searching for an accepting cycle, the single condition
necessary to decide it's existence is to find at least one previously visited
state from which the currently tested accepting state is reachable.

Let $G(V,E,L_{abels})$ be a graph where $V$ is a set of vertices, $E:V
\rightarrow V$ edges and $L_{abels}:V \rightarrow Int$ a random
assignment of a single integer value to each vertex $v \in V$. 
\begin{statement}
Let $\ge$ be a total order relation over $V$, then while resolving a transition
$s \rightarrow s'$ while searching for an accepting cycle in the graph $G$
using on-the-fly algorithm, we may store only such states $s'$ that meet
condition $s \ge s'$ without any impact on algorithm correctness.
\end{statement}

The correctness of this statement seems to be only partially correct. The 
Depth-First Search (DFS) algorithms such as the well known Nested-DFS
algorithm, seem to behave as expected without any further changes. Altering the
storing condition to the BFS algorithms seem to suffer from a slightly disrupted
behaviour that has to be corrected. In the following section the OWCTY algorithm
is analysed in detail and the necessary changes are pinpointed and explained.

At this point a very valid question might pop up. Is the technique presented
really useful, when algorithms themselves need to be altered to exploit it's
contribution? This is surely a legitimate concern and my answer to this
question would be yes, I still consider the technique to be universal, but at
this point, I would like to postpone an attempt to explain the reason after at
least one algorithm is examined in detail which would provide more essential
background to decide.

\subsection{altering OWCTY algorithm}

\begin{algorithm}
\caption{modified OWCTY}\label{alg:OWCTY}
\begin{algorithmic}[1]
\Procedure{OWCTY}{}
    \State \Call{Initialize}
    \Repeat
        \State $oldSize \gets |S|$
        \ForAll{$s \in V$} 
            \State $s.pre \gets \emptyset$
        \EndFor
        \State enqueue all states from $S \cap F$ into $q$
        \State \Call{Reachability}{}
        \State enqueue all states from $S \cap F$ into $q$
        \State \Call{Elimination}{}
    \Until{$|S|=oldSize$}
	\Return $|S| > 0$
\EndProcedure
\end{algorithmic}
\end{algorithm}


\begin{algorithm}
\caption{modified OWCTY}\label{alg:OWCTY:init}
\begin{algorithmic}[1]
\Procedure{Initialize}{}
    \State enqueue $init$ into $q$
    \While{$\neg q.empty$}
        \State $t \gets q.pop()$
        \If{$t \not\in S$}
            \If{hashCondition(t) $||$ is Final(t)} \Comment{$\longleftarrow$}
                \State add $t$ to $S$ \Comment{$\longleftarrow$}
            \EndIf
            \ForAll{$(t,u) \in E$}
                \State enqueue $u$ into $q$
            \EndFor
        \EndIf
    \EndWhile
\EndProcedure
\end{algorithmic}
\end{algorithm}


\begin{algorithm}
\caption{modified OWCTY}\label{alg:OWCTY:reach}
\begin{algorithmic}[1]
\Procedure{Reachability}{}
    \State $S \gets \emptyset$
    \While{$\neg q.empty$}
        \State $t \gets q.pop()$
        \If{$t \not\in S$}
            \If{hashCondition(t) $||$ isFinal(t)} \Comment{$\longleftarrow$}
                \State add $t$ to $S$ \Comment{$\longleftarrow$}
            \EndIf
            \ForAll{$(t,u)\in E$}
                \If{hashCondition(u) $||$ isFinal(u)} \Comment{$\longleftarrow$}
                    \State $u.pre \gets u.pre+1$ \Comment{$\longleftarrow$}
                \EndIf
                \State enqueue $u$ into $q$
            \EndFor
        \EndIf
    \EndWhile
\EndProcedure
\end{algorithmic}
\end{algorithm}

\begin{algorithm}
\caption{modified OWCTY}\label{alg:OWCTY:eliminate}
\begin{algorithmic}[1]
\Procedure{Elimination}{}
    \While{$\neg q.empty$}
        \State $t \gets q.pop()$
        \If{$t.pre \le 0$} \Comment{$\longleftarrow$}
            \State remove $t$ from $S$
            \ForAll{$(t,u) \in E$}
                \State $u.pre \gets u.pre - 1$
                \State enqueue $u$ into $q$
            \EndFor
        \EndIf
    \EndWhile
\EndProcedure
\end{algorithmic}
\end{algorithm}

The Algorithms \ref{alg:OWCTY},\ref{alg:OWCTY:init},\ref{alg:OWCTY:reach} and
\ref{alg:OWCTY:eliminate} demonstrates the behaviour of modified OWCTY algorithm.
All the lines that differ from the original algorithm are marked with an arrow.

The main algorithm \ref{alg:OWCTY} does not suffer any changes at all. The
lines 6-7 of algorithms \ref{alg:OWCTY:init} and \ref{alg:OWCTY:reach} contain
the crucial part that corresponds to the test for a \textit{hashCondition(u)},
which represents the comparison of the ordering defined on all the states of
the given graph. It is worth mentioning that the set $S$ corresponds to what
would be a hash table of states in any model checker implementing OWCTY
algorithm. Thus postponing the insertion of the certain state into the set $S$
reduces the amount of states that need to be stored.

On the line 11 of the \Call{Reachability} procedure the algorithm is slightly
modified to reflect certain changes in behaviour. The initial state $t$ of the
transition pair $(t,u)$ increases the number of predecessors only to those
states that are stored and always by the value of 1. If there are more than one
predecessors of $t$ and the $t$ is not stored, all the paths following the $t$
vertex are walked through again until at least one vertex representative  of
each cycle is stored and accumulates all the single vertex increments, thus
holding the correct number of predecessors when all the vertices from the queue
$q$ are processed.

Another change to the original algorithm needed to be made in the condition at
the line 4 of the \Call{Elimination} procedure. The reason is that the $t$ 
vertex in the Elimination phase is at that point stored only in the queue of
unprocessed vertices, hence it might not be stored in the hash table and in that
case we now allow to decrease an undefined predecessor counter to -1. Again as
in the case of the \Call{Reachability} procedure the negative vertex that is
not stored in the hash table may be inserted into the queue repeatedly with the
negative value assigned, but the succession of such decrements will, by
definition of the hashCondition, in finite number of steps affect one vertex
that is stored in the table and correctly adjust the number of predecessors.

At this point I would like to return to the question that surfaced before I
presented the algorithm. As we seen, the OWCTY algorithm had to be modified not
only by the storing condition, but also at two points the original definition
had to change the conditions to work correctly. But after closer examination,
one can see that the change to the lines 10-12 of \Call{reachability} procedure
is only an optimization and the change to the line 4 in the Algorithm
\ref{alg:OWCTY:eliminate} would be functional even without the impact of this
approach. The allowance of negative number is a simple generalisation of the
former condition that couldn't occure and thus the most unambiguous definition
was used.

\chapter{Conclusions}
The algorithm presented should provide certain memory usage reduction in trade
with the computational time. Sadly the implementation is not yet at such a phase
to be readily tested on real models. Few simple tests suggested that while using
one simple hash function to encode state ordering, the memory savings varied in
between 5 to 10\% ran in the DivInE model checker. Nevertheless, the algorithm
implemented still triggers various segmentation faults at the moment the
correctness of its implementation and results obtained can not be trusted yet.

The future work hence imply an attentive insight into the application structure
and correct inclusion of the algorithm, and of course test the product on various
models to compare the measurements with the original ie. nonmodified behaviour.

Further work may be aimed at choosing various functions to generate generally
better states ordering, and even combining multiple ordering mechanisms at once
to ensure as much state storing skips as possible. 

\printbibliography

\end{document}
